b:, f:(int_seg(0; b)).
(n:int_seg(0; b). ((f(n))))
 guard((((f(mu(f))))  (i:int_seg(0; b). (i < mu(f))  (((f(i))))))) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), guard(T), t  T, A, False, ge(i; j), A  B, int_seg(i; j), P  Q, lelt(i; j; k), prop{i:l}, subtype(S; T), suptype(S; T), mu(f), Y, if b then t else f fi , tt, ff, sq_type(T), T, True, , , Unit, P  Q, decidable(P), P  Q,
Lemmas	nat wf, int seg wf, assert wf, bool wf, nat properties, ge wf, mu wf, le wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, decidable int equal, squash wf, true wf, mu-bound